////////////////////////////////////////////////////////////////////////////////
// This file is part of the Mist compiler.                                    //
//                                                                            //
// Copyright (C) 2009 The Mist project                                        //
//                                                                            //
// For a list of contributors, see the COMMITTERS file.                       //
//                                                                            //
// The Mist compiler is free software: you can redistribute it and/or modify  //
// it under the terms of the GNU General Public License as published by       //
// the Free Software Foundation, either version 3 of the License, or          //
// (at your option) any later version.                                        //
//                                                                            //
// The Mist compiler is distributed in the hope that it will be useful,       //
// but WITHOUT ANY WARRANTY; without even the implied warranty of             //
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the              //
// GNU General Public License for more details.                               //
//                                                                            //
// You should have received a copy of the GNU General Public License          //
// in the COPYING file. If not, see <http://www.gnu.org/licenses/>.           //
////////////////////////////////////////////////////////////////////////////////

///
/// \file
/// Contains the interface to KeY-tool. Creates a proof of validity of a boolean
/// Mist-expression using KeY-tool.
///

#ifndef KEY_SOLVER_HPP
#define KEY_SOLVER_HPP

////////////////////////////////////////////////////////////////////////////////
// Includes                                                                   //
////////////////////////////////////////////////////////////////////////////////

#include "common/ptr.hpp"

#include <string>
using std::string;

////////////////////////////////////////////////////////////////////////////////
// Forward Declarations                                                       //
////////////////////////////////////////////////////////////////////////////////

class Expression;

namespace boost {
	namespace process {
		class child;
	}
}

////////////////////////////////////////////////////////////////////////////////
// KeySolver Class                                                            //
////////////////////////////////////////////////////////////////////////////////

/// Proofs validity of the given expression using KeY-tool. Expression must be
/// boolean. A temporary file containing the expression is created for KeY in
/// /tmp, and a file containing the proof is stored by KeY in /tmp.
///
class KeySolver {
	public:
		
		/// The status of the proof of the expression.
		///
		enum ProofStatus {
			FAILED = 0, ///< Used if the proof system has failed for some unknown reason.
			TIMEOUT,    ///< Used if the proof search exceeded the time limit.
			NOT_PROVED, ///< Used if a proof could not be found.
			PROVED      ///< Used if a proof has been found.
		};
		
		/// Attempt proof of validity of \a problem and set status. Temporary
		/// files containing the expression and its proof are stored in /tmp.
		///
		KeySolver(sptr<Expression> problem);
		
		/// \return the problem expression to prove
		///
		wptr<Expression> problem() const;
		
		/// Starts KeY-tool and attempts to prove the problem in problemfile.
		///
		void start_key();
		
		/// \return the contents of the proof file created by KeY
		///
		string report();
		
		/// \return the status of the KeY proof.
		///
		ProofStatus proof_status();
		
		/// \return the file-name of the proof file.
		///
		string proof_file();
	
	private:
		
		/// The path to KeY-tool.
		///
		static const string PathToKey;
		
		/// Time limit for the proof search in milliseconds.
		///
		static const uint TimeOut;
		
		/// \return a string of the form /tmp/key# (# is a number) where
		/// /tmp/key#.key is a file guaranteed not to exist.
		///
		string _tempFileName();
		
		/// The status of the proof of the expression.
		///
		enum KeyStatus {
			NOT_STARTED = 0, ///< KeY has not started the proof yet.
			BUSY,            ///< KeY is currently attempting to prove the problem.
			FINISHED         ///< KeY has finished execution.
		};
		
		/// Sets the proof status. Blocks while KeY has not finished execution.
		/// Starts KeY if necessary.
		///
		void _setProofStatus();
		
		sptr<Expression> _problem;
		sptr< ::boost::process::child> _process;
		ProofStatus _proofStatus;
		KeyStatus _keyStatus;
		string _problemFile;
};

#endif // KEY_SOLVER_HPP
